/**
 * 
 */
package extensionTools.smvCreator;

import java.util.ArrayList;
import java.util.Dictionary;
import java.util.Enumeration;
import java.util.HashSet;
import java.util.Hashtable;

import extensionTools.smvCreator.Link.LinkType;
import extensionTools.smvCreator.Link.SmvType;
import extensionTools.smvCreator.Exceptions.RulesUtilsException;
import extensionTools.smvCreator.Exceptions.SmvDBException;
import extensionTools.smvCreator.Exceptions.SmvInputException;

/**
 * This class implements the initialization of the system - declarations of
 * variables and their initial state
 * 
 * @author dani
 * 
 */
public class SystemInit extends Rule {
	/**
	 * This is the class constructor, all it does is send db to the father c'tor
	 * 
	 * @param db
	 */
	public SystemInit(DiagramDatabase db) {
		super(db);
	}

	/**
	 *  This would be the output initialization string
	 */
	private String initString;
	/**
	 *  This would be the output definition string
	 */
	private String defString;
	/**
	 * This would be the caseLine parameters for the transfer from sysState
	 * step2 to event1 (when no events occurred.
	 */
	private String allEvents;
	
	/**
	 * This is the next rules for the newly created instrument and condition 
	 * links
	 */
	private String fakeAssocs;
	// A set of all the evInvoke variables in the system
	private static HashSet<String> evInvokeVariables = new HashSet<String>();

	
	// an array containing all the assocs in the system, so we wouldn't have
	// them twice
	ArrayList<String> assocList = new ArrayList<String>();

	/**
	 * This function receives a database and creates the System variables
	 * declaration and initializations.
	 * 
	 * @param db
	 *            the system's Database
	 * @return a String in smv which implements the rule
	 * @throws SmvDBException
	 * @throws SmvInputException
	 * @throws RulesUtilsException
	 */
	@Override
	public String createRule() throws SmvInputException, SmvDBException,
			RulesUtilsException {
		defString = SmvOp.defVar("sysState",
				"{initial,event1,step1,phase1,event2,step2,terminated}")
				+ SmvOp.defVar("sysTerminate", defineIntArr(db.getSysTerm()))
				+ "\n";
		initString = SmvOp.init("sysState", "initial")
				+ SmvOp.init("sysTerminate", "1") + "\n";
		allEvents = SmvOp
				.and("sysState = step2", SmvOp.not("sysTerminate = 0"));// the
																		// step
																		// where
																		// we
																		// look
																		// for
																		// changes
		objectInit();
		procInit();
		String sysTerminate = sysTerminate();

		String[] rules = new String[9];
		rules[0] = SmvOp.createCaseLine("sysState = initial", "event1");
		rules[1] = SmvOp.createCaseLine("sysState = event1", "step1");
		rules[2] = SmvOp.createCaseLine(
				SmvOp.and("sysState = step1", SmvOp.not("sysTerminate = 0")),
				"phase1");
		rules[3] = SmvOp
				.createCaseLine(
						SmvOp.and("sysState = step1", "sysTerminate = 0"),
						"terminated");
		rules[4] = SmvOp.createCaseLine("sysState = phase1", "event2");
		rules[5] = SmvOp.createCaseLine("sysState = event2", "step2");
		rules[6] = SmvOp.createCaseLine(
				SmvOp.and("sysState = step2", allEvents), "event1");
		rules[7] = SmvOp.createCaseLine(
				SmvOp.and("sysState = step2", SmvOp.not(allEvents)), "event2");
		rules[8] = SmvOp.createCaseLine("sysState = terminated", "terminated");
		String sysStateNext = SmvOp.next("sysState", SmvOp.createCase(rules))
				+ "\n";

		return SmvOp.smvTemplate(defString, initString + sysStateNext + "\n"
				+ sysTerminate+"\n"+fakeAssocs, "");
	}

	/**
	 * This function defines the next case for sysTerminate event
	 * @throws RulesUtilsException - when null parameters were sent to SmvOp
	 */
	private String sysTerminate() throws RulesUtilsException {
		String arg = "sysState = event1 ";
		String res = SmvOp.prepareTerminationRes(db.getSysTerm());
		arg = SmvOp.createCaseLine(arg, res);
		res = SmvOp.createCaseLine("TRUE", "sysTerminate");
		return SmvOp.next("sysTerminate", SmvOp.createCaseS(arg, res));
	}

	/**
	 * This function init's association links created by a link from the system
	 * 
	 * @param link
	 *            - the Link we get data from
	 * @param db
	 *            - current diagramdatabase
	 */
	private void assocInit(Link link, int i, int j, boolean initState,
			Dictionary<String, String> assocDec) {
		if (link == null || db == null)
			return;
		String srcName = RulesUtils.getLinkEdgeName(link, db, true);
		String dstName = RulesUtils.getLinkEdgeName(link, db, false);
		if (srcName != null && dstName != null) {
			String assocStr = "assoc_" + srcName + "_" + i + "_" + dstName
					+ "_" + j;
			if (assocDec.get(assocStr) == null)
				assocDec.put(assocStr, String.valueOf(initState).toUpperCase());
		}
	}

	/**
	 * This function adds process declarations
	 * 
	 * @param db
	 * @throws SmvInputException
	 *             - when we found a link we're not suppose to get
	 * @throws SmvDBException
	 *             - when we got an ID of a process not in the system
	 * @throws RulesUtilsException
	 *             - when xor/or dictionary building encountered problems
	 */
	private void procInit() throws SmvInputException, SmvDBException,
			RulesUtilsException {
		ArrayList<SmvProcess> procList = db.getSmvProcessList();
		int evTerm = db.getEvTerm();
		for (SmvProcess smvProcess : procList) {
			xorAndOrInit(smvProcess);
			String procName = smvProcess.getName();
			for (int i = 0; i < SMVCreator.K; i++) {
				defString += SmvOp.defVar(procName + "_" + i,
						"{notActive,waiting,active}") + "\n";
				initString += SmvOp.init(procName + "_" + i, "notActive")
						+ "\n";
				initEvent("ev_activate_" + procName + "_" + i, false, false);
				initEvent("ev_wait_" + procName + "_" + i, false, false);
				initEvent("ev_halt_" + procName + "_" + i, false, false);

				// Termination is a special kind of event, the initEvent
				// function can't be used...
				defString += SmvOp.defVar("ev_terminate_" + procName + "_" + i,
						defineIntArr(evTerm)) + "\n";
				initString += SmvOp.init("ev_terminate_" + procName + "_" + i,
						"1") + "\n";
				allEvents = SmvOp.and(allEvents, SmvOp.not("ev_terminate_"
						+ procName + "_" + i + " = 0"));
				// Init's links where the process is the source
				ArrayList<Link> procLinkList = smvProcess.getLinkList();
				for (Link link : procLinkList) {
					long srcId = link.getSrcId();
					if (srcId == smvProcess.getId()) {
						LinkType lnkType = link.getLinkType();
						String dstName = RulesUtils.getLinkEdgeName(link, db,
								false);
						String event = "ev_";
						switch (lnkType) {
						case INVOCATION:
							event += "invoke_";
							// the destination process name
							String dstProc = RulesUtils.getLinkEdgeName(link,
									db, false);
							if (dstProc == null)
								throw new SmvDBException(
										"SystemInit: unknown destination in invokation from "
												+ procName);
							break;
						default:
							event = null;
						}
						// initializing the event

						if (event != null)
							initEvent(event + procName + "_" + i + "_"
									+ dstName, true, false);
					}
				}
			}
		}
	}

	/**
	 * This function inits all or/xor events of a certain process
	 * 
	 * @param proc
	 *            - the process which is the source
	 * @throws RulesUtilsException
	 *             - when there was trouble with constructing or/xor information
	 * @throws SmvDBException
	 *             - when there are unexpected destinations in the links
	 */
	private void xorAndOrInit(SmvProcess proc) throws RulesUtilsException,
			SmvDBException {
		// first we do the ors
		ArrayList<ArrayList<Link>> orLists = proc.getOrLists();
		for (ArrayList<Link> or : orLists) {
			ArrayList<String> objs;
			try {
				objs = RulesUtils.getDstNames(or,db);
			} catch (SmvDBException e) {
				throw new SmvDBException("SystemInit: problem with or lists at "
						+ proc.getName());
			}
			Dictionary<String, String> evOrs = RulesUtils.getXorDict(
					proc.getName(), objs, false);
			Enumeration<String> names = evOrs.keys();
			while (names.hasMoreElements()) {
				String name = names.nextElement();
				initString += SmvOp.init(name, "false");
				defString += SmvOp.defVar(name, "{" + evOrs.get(name) + "}");
				allEvents = SmvOp.and(allEvents, name + "= false");
			}
		}
		// now, we init the Xors
		ArrayList<ArrayList<Link>> xorLists = proc.getXorLists();
		for (ArrayList<Link> xor : xorLists) {
			ArrayList<String> objs;
			try {
				objs = RulesUtils.getDstNames(xor,db);
			} catch (SmvDBException e) {
				throw new SmvDBException("SystemInit: problem with xor lists at "
						+ proc.getName());
			}
			Dictionary<String, String> evXors = RulesUtils.getXorDict(
					proc.getName(), objs, true);
			Enumeration<String> names = evXors.keys();
			while (names.hasMoreElements()) {
				String name = names.nextElement();
				initString += SmvOp.init(name, "false");
				defString += SmvOp.defVar(name, "{" + evXors.get(name) + "}");
				allEvents = SmvOp.and(allEvents, name + "= false");
			}
		}
	}

	/**
	 * This function adds object declarations
	 * 
	 * @param db
	 * @throws SmvInputException
	 *             - when we found too many instances of the same object
	 * @throws SmvDBException
	 *             - when we couldn't find a state in the object who should be
	 *             there or got unexpected srcType in a link or couldn't find a
	 *             process which acts in a link or an object tried to be a
	 *             source of an instantiation link
	 * @throws RulesUtilsException - when something is wrong in SmvOp
	 */
	private void objectInit() throws SmvInputException, SmvDBException, RulesUtilsException {
		if (db == null)
			return;
		Dictionary<String, SmvProcess> specialLinks = new Hashtable<String, SmvProcess>();
		Dictionary<String, ArrayList<SmvInstanceObject>> initialObj = getInstances();
		ArrayList<SmvObject> objList = db.getSmvObjectList();
		for (SmvObject smvObject : objList) {
			String states = RulesUtils.getStateNames(smvObject);
			String objName = smvObject.getName();
			Dictionary<String, String> objToObjAssoc = new Hashtable<String, String>();
			ArrayList<Link> links = smvObject.getLinkList();
			ArrayList<SmvInstanceObject> currInsts = initialObj.get(objName);
			ArrayList<String> structuralLinks = new ArrayList<String>();
			// here we init all object instances, and return the number of the
			// next left to init
			int objLeft = initObjInstances(currInsts, objToObjAssoc);
			// in case there were too many instances
			if (-1 == objLeft) {
				throw new SmvInputException("SystemInit: Too many instances of object "
						+ objName);
			}
			for (int i = 0; i < SMVCreator.K; i++) {
				// init's the smvObject
				defString += SmvOp
						.defVar(objName + "_" + i, "{" + states + "}") + "\n";
				// should've been initialized as an instance
				if (i >= objLeft) {
					initString += SmvOp.init(objName + "_" + i, "notExist")
							+ "\n";
				}

				// if the object is environmental, we want to be able to create
				// it by lottory
				if (smvObject.isEnvironmental()) {
					State initialState = smvObject.getInitialState();
					String linkName;
					if(initialState != null) linkName = "ev_create_" + objName + "_" + i + "_"+initialState.getName();
					else linkName = "ev_create_" + objName + "_" + i;
					//This link is handled only in step1, therefor not included in "allEvents"
					defString += SmvOp.defVar(linkName,	defineIntArr(db.getCreationVar()));
					initString += SmvOp.init(linkName,"1");
				}

				// init's the smvObject events
				for (Link link : links) {
					String specialLinkName = null;
					String linkName = "";
					long src = link.getSrcId();
					long dst = link.getDstId();
					State state = null;
					SmvProcess proc = null;
					// setting the link init
					switch (link.getLinkType()) {
					case RESULT:
						if (link.getSrcType() != SmvType.PROCESS)
							throw new SmvDBException("SystemInit: Unexpected link srcType "
									+ linkName);
						// we would prefer using get_byId than getLinkEdgebyId
						proc = RulesUtils.getProccessbyId(src, db);
						if (proc == null)
							throw new SmvDBException("SystemInit: Proc missing in link "
									+ linkName);
						String procName = proc.getName();
						if (link.getDstType() == SmvType.STATE) {
							state = smvObject.idBelongsToObj(dst);
							if (state == null)
								throw new SmvDBException(
										"SystemInit: State doesn't exist in Object "
												+ objName);
							linkName += state.getName() + "_";
						}
						//The object would be created in initial state
						// if one exists
						else{
							state= smvObject.getInitialState();  
							if(state!=null) linkName += state.getName() + "_";
						}
						
						String stateName = (state == null) ? null : state
								.getName();
						// if the link has a label it means he's not
						// a result link, but part of a effect link.
						if (link.getLabel() == "") {
							// this function would handle evCreate init, because
							// it's a
							// special event the way I programmed it, and can't
							// be init by
							// a simple call to initEvent
							if (i == 0)
								initEvCreate(objName, procName, stateName);
						}
						// we add the link to a dictionary
						else {
							// modify already installed in result
							continue;
						}
						// adding association to the father of proc
						fatherAssoc(objName + "_" + i,
								RulesUtils.getProccessbyId(proc.getFatherId(),
										db), true, "");

						break;

					case CONSUMPTION:
						boolean procSrcFlag = false;
						linkName = "ev_consumption_" + objName + "_" + i + "_";

						if (link.getSrcType() == SmvType.STATE) {
							state = smvObject.idBelongsToObj(src);
							if (state == null)
								throw new SmvDBException(
										"SystemInit: State doesn't exist in Object "
												+ objName);
							linkName += state.getName() + "_";
						}

						if (link.getDstType() != SmvType.PROCESS)
							throw new SmvDBException("SystemInit: Unexpected link dstType "
									+ linkName);
						// we would prefer using get_byId than getLinkEdgebyId
						proc = RulesUtils.getProccessbyId(dst, db);
						if (proc == null)
							throw new SmvDBException("SystemInit: Proc missing in link "
									+ linkName);
						// if link has a label he's not a consumption link, but
						// part of
						// an effect link.
						if (link.getLabel() == "") {
							linkName +=  proc.getName();
							initEvent(linkName, true, false);
													}
						else {
							//in modify, the proc.
							procSrcFlag=true;
							linkName = "ev_modify_" + objName + "_" + i + "_"
							+ proc.getName();
							State dstState = db.getNextUpdate(state, link.getLabel());
							if(dstState == null) throw new SmvDBException("SystemInit: No dest. state found on "+linkName);
							for (int j = 0; j < SMVCreator.K; j++) {
								initEvent(linkName + "_" + j + "_" + state.getName()
										+ "_" + dstState.getName(), false, false);
							}
						}
							fatherAssoc(
									objName + "_" + i,
									RulesUtils.getProccessbyId(
											proc.getFatherId(), db), procSrcFlag, "");

						// adding association to the father of proc
						break;
					// The object has a relation with procs, but isn't consumed
					case CONDITION:
						if (specialLinkName == null)
							specialLinkName = "Condition";
					case INSTRUMENT:
						if (specialLinkName == null)
							specialLinkName = "Instrument";

						proc = RulesUtils.getProccessbyId(dst, db);
						if (proc == null)
							throw new SmvDBException("SystemInit: Proc missing in link "
									+ linkName);
						// there's no event link here, we would know of this one
						// only
						// through the assoc with the father.
						fatherAssoc(objName + "_" + i,
								RulesUtils.getProccessbyId(proc.getFatherId(),
										db), false, specialLinkName);
						//to insert the new links special variable
						if(specialLinks.get(SmvOp.setFirstCharToLowerCase(specialLinkName)+"_"+objName) == null)
							specialLinks.put(SmvOp.setFirstCharToLowerCase(specialLinkName)+"_"+objName, proc);
						
						break;
					case EFFECT:
						proc = RulesUtils.getProccessbyId(dst, db);
						if (proc == null)
							throw new SmvDBException("SystemInit: No Proccess found in modify link at "+smvObject);
						//in case there are not enough states per object for update
						if(smvObject.getStateList().size() <= 1){
							throw new SmvInputException("SystemInit: Can't use effect link on object with no states "+objName);
						}
						linkName = "ev_modify_" + objName + "_" + i + "_"
								+ proc.getName();
						ArrayList<State> objStates = smvObject.getStateList();
						for(int j=0;j<SMVCreator.K;j++){
							for (State st : objStates) {
								initEvent(linkName+"_"+j+"_"+st.getName(), false, false);
							}
						}
						fatherAssoc(objName + "_" + i,
								RulesUtils.getProccessbyId(proc.getFatherId(),
										db), true, "");
						break;
					// all of these links are relations of ASSOC between two
					// objects
					// it would retain similar attributes in the state machine,
					// apart
					// from CHARACTERIZATION, which would play a bit differently
					// in the next of objects
					case CHARACTERIZATION:
					case PARTICULATION:
					case BIDIRECTIONAL:
					case UNIDIRECTIONAL:

						if (smvObject.getId() == src) {
							if (link.getDstType() != SmvType.OBJECT)
								throw new SmvDBException(
										"SystemInit: Object missing in link" + linkName);
							SmvObject dstObj = RulesUtils
									.getObjectbyId(dst, db);
							if (dstObj == null)
								throw new SmvDBException(
										"SystemInit: Object missing in link " + linkName);
							// Assoc init is here iff the object has no
							// instances in the diagram
							for (int j = 0; j < SMVCreator.K; j++) {
								String temp = "assoc_" + objName + "_" + i
										+ "_" + dstObj.getName() + "_" + j;
								defString += SmvOp.defVar(temp, "boolean");
								if (!structuralLinks.contains(temp))
									structuralLinks.add(temp);
							}
						}
						break;
					case INSTANTIATION:
						break;
					}
				}
			}
			assocList.clear();
			initStructuralLinks(structuralLinks, objToObjAssoc);
		}
		initSpecialLinks(specialLinks);
	}

	/**
	 * This function inits the special links in the system (instument and condition)
	 * and makes their "cases"
	 * @param specialLinks
	 * @throws RulesUtilsException - if some error in SmvOp happened 
	 * @throws SmvInputException - if some error in the process happened
	 */
	private void initSpecialLinks(Dictionary<String, SmvProcess> specialLinks) throws RulesUtilsException, SmvInputException {
		Enumeration<String> keys = specialLinks.keys();
		fakeAssocs="";
		while (keys.hasMoreElements()) {
			String key = keys.nextElement();
			for(int i = 0; i<SMVCreator.K ; i++){
				SmvProcess proc = specialLinks.get(key);
				if(proc == null ){
					throw new SmvInputException("SystemInit: No proccess found for variable "+key);
				}
				String name = key +"_"+i+"_"+ proc.getName()+"_"+i;
				//these links act like assocs
				initEvent(name, true, false);
				fakeAssocs+= SmvOp.next(name+"_"+i,SmvOp.createCaseS(SmvOp.createCaseLine(proc.getName()+"_"+i+"=active", "TRUE"),
							 SmvOp.createCaseLine("TRUE","FALSE")));
			}	
		}
	}

	/**
	 * This function checks if we initialized the structural link (appears in
	 * dictionary) and init FALSE otherwise
	 * 
	 * @param structuralLinks
	 *            - all instantiations of smvObj structural links
	 * @param objToObjAssoc
	 *            - a dictionary of all previous initializations to update
	 *            (usually because of instantiations
	 */
	private void initStructuralLinks(ArrayList<String> structuralLinks,
			Dictionary<String, String> objToObjAssoc) {
		for (String string : structuralLinks) {
			String val = objToObjAssoc.get(string);

			if (val == null)
				initString += SmvOp.init(string, "FALSE");
			else
				initString += SmvOp.init(string, val);

		}
	}

	/**
	 * This function creates and inits the ev_create link
	 * 
	 * @param objName
	 * @param procName
	 * @param stateName
	 *            - null if the link is not between a process to a state
	 */
	private void initEvCreate(String objName, String procName, String stateName) {
		String linkName = "ev_create_";
		// creating the "class" event - choose an instance
		// and an event for each instance
		for (int i = 0; i < SMVCreator.K; i++) {
			if (stateName == null)
				initClassEvent(linkName + procName + "_" + i + "_" + objName);
			else
				initClassEvent(linkName + procName + "_" + i + "_" + objName
						+ "_" + stateName);
			for (int j = 0; j < SMVCreator.K; j++) {
				linkName += procName + "_" + i + "_" + objName + "_" + j;
				// in case the event is for a special state.
				if (stateName != null)
					linkName += "_" + stateName;
				initEvent(linkName, false, false);
				linkName = "ev_create_";
			}
		}
	}

	/**
	 * This method creates the ev_create of an object (the variable that choose
	 * which instance to create
	 * 
	 * @param string
	 *            - the event full name
	 */
	private void initClassEvent(String string) {
		String enumer = "{false";
		for (int i = 0; i < SMVCreator.K; i++)
			enumer += "," + i;
		initString += SmvOp.init(string, "false");
		defString += SmvOp.defVar(string, enumer + "}");
		// this event happens only in Phases and therefore not interesting for
		// the transition
		// from step2 to event1 , so We didn't put him in the "allEvents" string
	}

	/**
	 * This function initialize the instances of objects
	 * 
	 * @param initialObj
	 *            - array of all instantiations of an object
	 * @param objToObjAssoc
	 * @return the number of the next instance (who should be notExist at the
	 *         begining
	 * @throws SmvDBException
	 *             - in case of unexpected instance or some unexpected link edge
	 */
	private int initObjInstances(ArrayList<SmvInstanceObject> initialObj,
			Dictionary<String, String> objToObjAssoc) throws SmvDBException {
		if (initialObj == null)
			return 0;// i.e. no instances
		int objLeft = initialObj.size();
		// in case too many instantiations were created
		if (objLeft > SMVCreator.K)
			return -1;
		int i = 0;
		String objName = initialObj.get(0).getFatherInstanceName();
		for (SmvInstanceObject inst : initialObj) {
			ArrayList<Link> linkList = inst.getLinkList();
			State initialState = inst.getInitialState();
			if (initialState == null) {
				// getting states without notExist
				String states = RulesUtils.getStateNames(inst).replaceAll(
						",notExist", "");
				initString += SmvOp.init(objName + "_" + i, "{" + states + "}")
						+ "\n";
			} else
				initString += SmvOp.init(objName + "_" + i,
						initialState.getName())
						+ "\n";

			for (Link link : linkList) {
				// in case or wrong model building
				if (link.getLinkType() == LinkType.INSTANTIATION
						&& link.getSrcId() == inst.getId())
					throw new SmvDBException(
							"SystemInit: SmvInstanceObject can't be a source in an instantiation link"
									+ objName);
				if ((link.getLinkType() == LinkType.PARTICULATION || link
						.getLinkType() == LinkType.CHARACTERIZATION)
						&& link.getSrcId() == inst.getId()) {
					// in init the instances would have the same instance number
					assocInit(link, i, i, true, objToObjAssoc);
				}
			}
			i++;
		}
		// This would return the next instance's Number (one that hasn't been
		// initialized
		return i;
	}

	/**
	 * This function find and inserts to a dictionary the instances, the key is
	 * the object name, and the value is an arrayList of the instances
	 * 
	 * @return a dictionary as described above
	 */
	private Dictionary<String, ArrayList<SmvInstanceObject>> getInstances() {
		ArrayList<SmvInstanceObject> allInst = db.getSmvInstanceObjectList();
		Dictionary<String, ArrayList<SmvInstanceObject>> instDict = new java.util.Hashtable<String, ArrayList<SmvInstanceObject>>();
		for (SmvInstanceObject currInst : allInst) {
			String currObjName = currInst.getFatherInstanceName();
			// getting the instance list for the object from dict, if such
			// exist.
			ArrayList<SmvInstanceObject> instList = instDict.get(currObjName);
			if (null == instList) {
				// creating a new list for the object
				instList = new ArrayList<SmvInstanceObject>();
				instList.add(currInst);
			} else
				instList.add(currInst);
			// inserting the object to the dictionary with the new list
			instDict.put(currObjName, instList);
		}
		return instDict;
	}

	/**
	 * This function create the father-of-process to object associations
	 * 
	 * @param objName
	 *            - the object
	 * @param father
	 *            - the process father
	 * @param isProcSrc
	 *            if the process should be the source in this link
	 * @param linkName
	 *            - the name of the link (in case we want to add it)
	 * @throws SmvDBException
	 *             - in case of father missing
	 */
	private void fatherAssoc(String objName, SmvProcess father,
			boolean isProcSrc, String linkName) throws SmvDBException {
		if (father == null)
			throw new SmvDBException(
					"SystemInit: Proc father missing for father association with" + objName);
		String fatherName = father.getName();
		// the case of no link name is required
		if (linkName == null)
			linkName = "";
		// FIXED
		for (int j = 0; j < SMVCreator.K; j++) {
			if (isProcSrc)
				initEvent("assoc" + linkName + "_" + fatherName + "_" + j + "_"
						+ objName, false, true);
			else
				initEvent("assoc" + linkName + "_" + objName + "_" + fatherName
						+ "_" + j, false, true);
		}
	}

	/**
	 * This function init's the system events
	 * 
	 * @param linkName
	 *            - event name
	 * @param needs_renumbering
	 *            - in case there's another entity in play, also with K
	 *            instances
	 * @param isAssoc
	 *            - if this event is assoc, no need to check it for system
	 *            termination
	 */
	private void initEvent(String linkName, boolean needs_renumbering,
			boolean isAssoc) {
		if (needs_renumbering) {
			for (int i = 0; i < SMVCreator.K; i++) {
				// associations doesn't count as events for the SysState machine
				// algorithm
				if (!isAssoc)
					allEvents = SmvOp.and(allEvents, linkName + "_" + i
							+ "= FALSE");
				else {
					// to prevent the same Assoc coming from two different links
					if (assocList.contains(linkName + "_" + i))
						return;

				}

				// should not happen iff we initialized an object
				if (!initString.contains(linkName + "_" + i))
					initString += SmvOp.init(linkName + "_" + i, "FALSE")
							+ "\n";
				defString += SmvOp.defVar(linkName + "_" + i, "boolean") + "\n";
				//we don't want the fake vars here
				if(!(linkName.startsWith("condition") || linkName.startsWith("instrument")))
						evInvokeVariables.add(linkName + "_" + i);
				if (isAssoc)
					assocList.add(linkName + "_" + i);

			}
		} else {
			if (!isAssoc)
				allEvents = SmvOp.and(allEvents, linkName + "= FALSE");
			else {
				// to prevent the same Assoc coming from two different links
				if (assocList.contains(linkName))
					return;
			}
			initString += SmvOp.init(linkName, "FALSE") + "\n";
			defString += SmvOp.defVar(linkName, "boolean") + "\n";
			if (isAssoc)
				assocList.add(linkName);

		}
	}

	/**
	 * This function defines Smv array of ints, from zero to param.
	 * 
	 * @param param
	 *            - the right border of the array
	 * @return a String representing the arrau definition
	 */
	private String defineIntArr(int param) {
		if (1 >= param)
			return "0";
		return "0.." + param;
	}

	/**
	 * 
	 * @return the hash set which includes the evInvoke variables
	 */
	public static HashSet<String> getInvokeVariables() {
		return evInvokeVariables;
	}

}
